module Zeno.Clause where

import Prelude ()
import StdImports
import Zeno.Term

data Clause a
  = Clause  { clauseVariables :: ![a],
              clauseEquality :: !(Equality a),
              clauseConditions :: ![Equality a] }
  deriving ( Eq, Ord )
              
type Equality a = (Term a, Term a)

instance NFData a => NFData (Clause a) where
  rnf (Clause vars eq conds) = rnf vars `seq` rnf eq `seq` rnf conds
  
flipClauseEquality :: Clause a -> Clause a
flipClauseEquality cs = cs 
  { clauseEquality = flipPair (clauseEquality cs) }

addCondition :: Equality a -> Clause a -> Clause a
addCondition eq cs = cs 
  { clauseConditions = eq : (clauseConditions cs) }
  
instance Functor Clause where
  fmap f (Clause vs t cs) =
    Clause (map f vs) (mapEq t) (map mapEq cs) 
      where mapEq (l, r) = (fmap f l, fmap f r)
    
instance Foldable Clause where
  foldMap f (Clause vs t cs) = 
    foldMap f vs `mappend` f' t `mappend` mconcat (map f' cs)
      where f' (l, r) = foldMap f l `mappend` foldMap f r
    
instance Traversable Clause where
  sequenceA (Clause vs t cs) = 
    Clause <$> sequenceA vs <*> 
      sequence' t <*> sequenceA (map sequence' cs)
    where sequence' (l, r) = (,) <$> sequenceA l <*> sequenceA r

instance TermTraversable Clause where
  mapTermsM f (Clause vars eq conds) = do
    eq' <- mapPairM (mapTermsM f) eq
    conds' <- mapM (mapPairM (mapTermsM f)) conds
    return (Clause vars eq' conds')
    
showEquality :: Show a => (a, a) -> String
showEquality (l, r) = 
  let (l', r') = (show l, show r)
  in case r' of
       "True" -> l'
       "False" ->
         if ' ' `elem` l' 
           then "not (" ++ l' ++ ")"
           else "not " ++ l'
       _ -> l' ++ " = " ++ r'
  
instance Show a => Show (Clause a) where
  show (Clause vs t []) = showEquality t
  show (Clause vs t cs) = showEquality t ++ " :- " 
    ++ intercalate ", " (map showEquality cs)
